(declare-const v1 Bool)
(declare-const v9 Bool)
(declare-const i0 Int)
(declare-const i1 Int)
(declare-const i6 Int)
(declare-const i7 Int)
(declare-const i10 Int)
(declare-const r1 Real)
(declare-const v19 Bool)
(declare-const i12 Int)
(assert (or (= 0 i6) v1))
(assert (< i12 0 798))
(assert (or (<= i10 23) (>= 8999883.0 0.1653 r1)))
(assert (or (= i10 0) (= (* (- i6 i6 i1 i0 23) i6) i6)))
(assert (or (= i10 i1) (=> (=> v9 (> i6 9 i1 53 i7)) v19)))
(assert (or (distinct (to_int (* (+ (- r1) 45106.0 (- 8999883.0) 8999883.0 (- 8999883.0)) 45106.0 (+ r1 8999883.0 45106.0 45106.0) (+ (- r1) 45106.0 (- 8999883.0) 8999883.0 (- 8999883.0)) 4.0)) 882) v9))
(check-sat)
